Problem:
 f(s(X)) -> f(X)
 g(cons(0(),Y)) -> g(Y)
 g(cons(s(X),Y)) -> s(X)
 h(cons(X,Y)) -> h(g(cons(X,Y)))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {6,5,4}
   transitions:
    h1(8) -> 6*
    g1(7) -> 8*
    g1(2) -> 8,5
    g1(1) -> 8,5
    g1(3) -> 8,5
    cons1(3,1) -> 7*
    cons1(3,3) -> 7*
    cons1(1,2) -> 7*
    cons1(2,1) -> 7*
    cons1(2,3) -> 7*
    cons1(3,2) -> 7*
    cons1(1,1) -> 7*
    cons1(1,3) -> 7*
    cons1(2,2) -> 7*
    s1(2) -> 8,5
    s1(1) -> 8,5
    s1(3) -> 8,5
    f1(2) -> 4*
    f1(1) -> 4*
    f1(3) -> 4*
    f0(2) -> 4*
    f0(1) -> 4*
    f0(3) -> 4*
    s0(2) -> 1*
    s0(1) -> 1*
    s0(3) -> 1*
    g0(2) -> 5*
    g0(1) -> 5*
    g0(3) -> 5*
    cons0(3,1) -> 2*
    cons0(3,3) -> 2*
    cons0(1,2) -> 2*
    cons0(2,1) -> 2*
    cons0(2,3) -> 2*
    cons0(3,2) -> 2*
    cons0(1,1) -> 2*
    cons0(1,3) -> 2*
    cons0(2,2) -> 2*
    00() -> 3*
    h0(2) -> 6*
    h0(1) -> 6*
    h0(3) -> 6*
  problem:
   
  Qed